EOrder{i:l}  Type{i'} 

latex

Definitions	t  T, EventsWithOrder, x:A. B(x),
Lemmas	deq wf, unit wf, Id wf, top wf, IdLnk wf, EOrderAxioms wf